r,s:rationals. (r * s)  rationals 

latex

Definitions	prop{i:l}, guard(T), P  Q, sq_type(T), top, qeq(r; s), nequal(T; a; b), ff, tt, if b then t else f fi , r * s, int_nzero, b-union(A; B), t  T, rationals, x:A. B(x), P  Q, P  Q, P  Q,
Lemmas	assert of eq int, eq int wf, eqtt to assert, isint-int, nequal wf, mul nzero, bfalse wf, int nzero wf, ifthenelse wf, rationals wf, btrue wf, qeq wf, bool wf